A:Type, f:(A(A + Top)).
SWellFounded(p-graph(A;f)(y,x))
 p-inject(A;A;f)
 (x, y:A.
 (final-iterate(f;x) = final-iterate(f;y)  A)
  (n:. ((p-graph(A;f^n)(x,y))  (p-graph(A;f^n)(y,x))))) 

latex

Definitions	x:A. B(x), Top, P  Q, p-graph(A;f), x:A. B(x), P  Q, A c B, t  T, {T}, , S  T, suptype(S; T), x,y. t(x;y), True, , T, p-inject(A;B;f), P & Q, A, Dec(P), A  B, False, x(s1,s2)
Lemmas	final-iterate-property, decidable le, can-apply-fun-exp, can-apply-fun-exp-add, p-fun-exp-injection, do-apply wf, p-fun-exp wf, assert wf, can-apply wf, top wf, final-iterate wf, p-inject wf, strongwellfounded wf, p-graph wf2, le wf, squash wf, true wf, bool wf, nat wf